<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" 
    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
    <head>
        <title>InvariantJ - Class Invariants for Java</title>
        <link rel="stylesheet" href="style.css" type="text/css"/>
        <meta http-equiv="content-type" content="text/html; charset=utf-8"/>
        <meta name="author" content="Lance Walton" lang="en-uk"/>
    </head>
    <body>
        <div class="main">
            <div class="pageTitle">InvariantJ</div>
            <div class="contents">
                <div class="contentsTitle">Contents</div>
                <ul>
                    <li>
                        <a href="#introduction" title="A brief introduction to InvariantJ">Introduction</a>
                    </li>
                    <li>
                        <a href="#what" title="A quick overview of class invariants">What are Class Invariants?</a>
                    </li>
                    <li>
                        <a href="#implementing" title="Implementing invariants with InvariantJ">Implementing 
                            Invariants</a>
                    </li>
                    <li>
                        <a href="#compiling" title="How to compile and instrument your classes for invariant checking"> 
                            Compiling / Instrumenting</a>
                    </li>
                    <li>
                        <a href="#ide" title="Using InvariantJ with IDEs">Using InvariantJ with IDEs</a>
                    </li>
                    <li>
                        <a href="#wherePrecisely" title="Where precisely are invariants checked">Where Precisely are 
                            Invariants Checked</a>
                    </li>
                    <li>
                        <a href="#versions" title="A list of versions of software discussed in this page">Software 
                            Versions</a>
                    </li>
                    <li>
                        <a href="license.txt" title="MIT license for InvariantJ">License</a>
                    </li>
                </ul>
            </div>
            <div class="sectionHeading">
                <a name="introduction">Introduction</a>
            </div>
            <p>InvariantJ is a mechanism for implementing class invariant checking in Java. It uses a simple method 
                naming convention to allow developers to create as many invariants as they wish. If one or more 
                invariants fail at runtime, an exception will be thrown with a message containing the full list of 
                violated invariants.</p>
            <div class="sectionHeading">
                <a name="what">What are Class Invariants?</a>
            </div>
            <p>Class invariants are a major part of the Design by Contract technique. For a good discussion of this, 
                see Bertrand Meyer's &#8216;<a href="http://www.amazon.com/exec/obidos/ASIN/0136291554" 
                title="Bertrand Meyer's &#8216;Object Oriented Software Construction&#8217; at Amazon">Object 
                Oriented Software Construction</a>&#8217;. Whether or not Design by Contract is applied, specifying 
                invariants of classes in any system is useful in at least three ways:</p>
            <ul>
                <li>Invariants promote &#8216;fail fast&#8217; behaviour&nbsp;&#8211; <span class="latin">i.e.</span> 
                    if an unexpected condition arises, it is reported as early as possible</li>
                <li>Invariants convey deep semantic information about the class which results in greater 
                    maintainability at the very least and probably less code in clients due to greater 
                    knowledge about the state space of instances of the class</li>
                <li>Invariants are executable documentation</li>
            </ul>
            <p>Simply put, a class invariant is something that must be true about any instance of the class when that 
                instance is in a quiescent state. If an object is quiescent and one of its invariants is violated, it 
                usually means that there is a coding error in the class or in its hierarchy.</p>
            <p>Objects are quiescent when none of their behaviours are in the process of executing. If a behaviour is 
                executing, an invariant may be temporarily violated, to be restored subsequently before a quiescent 
                state is reached again.</p>
            <p>This is analagous to integrity constraints in an RDBMS which must hold on both sides of a transaction 
                but are not required to hold during the transaction.</p>
            <div class="subSectionHeading">How is this Different from Pre-Conditions and Post-Conditions</div>
            <p>A class invariant is a kind of pre- and post-condition. However, pre- and post-conditions apply to 
                single behaviours only and typically verify that parameters are appropriate, that the object's state is 
                suitable for the execution of the particular behaviour or that the results of execution are as 
                expected. A class invariant specifies both pre- and post conditions for all relevant behaviours but is 
                only tested just before an object leaves a quiescent state and just after it returns to one.</p>
            <div class="sectionHeading">
                <a name="implementing">Implementing Class Invariants</a>
            </div>
            <p>InvariantJ allows any class to easily specify invariants. All that is required is the addition of one or 
                more methods that conform to a naming convention and a signature. An invariant checking method must:</p>
            <ul>
                <li>have a name beginning with &#8216;<span class="code">isInvariant</span>&#8217;</li>
                <li>have a <span class="code keyword">boolean</span> return type</li>
                <li>take no parameters</li>
                <li>return <span class="code keyword">true</span> if the invariant is satisfied and <span 
                    class="code keyword">false</span> otherwise</li>
            </ul>
            <p>Here is an example:</p>
            <ul class="codeBlock">
                <li><span class="keyword">public class</span> FooBar {</li>
                <li>&nbsp;&nbsp;<span class="keyword">private</span> Foo <span class="variable">foo</span>;</li>
                <li>&nbsp;&nbsp;<span class="keyword">private</span> Bar[] <span class="variable">bar</span>;</li>
                <li>&nbsp;&nbsp;<span class="keyword">private</span> Baz[] <span class="variable">baz</span>;</li>
                <li>&nbsp;</li>
                <li>&nbsp;&nbsp;&#8230;</li>
                <li>&nbsp;</li>
                <li>&nbsp;&nbsp;<span class="keyword">protected boolean</span> isInvariantFoo() {</li>
                <li>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span> <span class="variable">foo</span> != 
                    <span class="keyword"> null</span>;</li>
                <li>&nbsp;&nbsp;}</li>
                <li>&nbsp;</li>
                <li>&nbsp;&nbsp;<span class="keyword">protected boolean</span> isInvariantBar() {</li>
                <li>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span> <span class="variable">bar</span> != 
                    <span class="keyword">null</span> &amp;&amp; <span class="variable">bar</span>.length >= 2;</li>
                <li>&nbsp;&nbsp;}</li>
                <li>&nbsp;</li>
                <li>&nbsp;&nbsp;<span class="keyword">protected boolean</span> isInvariantBaz() {</li>
                <li>&nbsp;&nbsp;&nbsp;&nbsp;<span class="keyword">return</span> <span class="variable">baz</span> == 
                    <span class="keyword">null</span> || <span class="variable">baz</span>.length == <span 
                    class="variable">bar</span>.length * 2;</li>
                <li>&nbsp;&nbsp;}</li>
                <li>}</li>
            </ul>
            <p>Invariant checking methods can have any visibility. However, visibility of at least <span 
                class="keyword">protected</span> is recommended since it allows subclasses to override the 
                invariant.</p>
            <p>At the entry and&nbsp;/&nbsp;or exit of appropriate behaviours, all invariant methods are invoked. After 
                all invariants have been checked, if any violations have occurred, an <span 
                class="code">com.stateofflow.invariantj.InvariantViolationError</span> is thrown with a message containing 
                information about all invariant violations.</p>
            <div class="sectionHeading">
                <a name="compiling">Compiling / Instrumenting</a>
            </div>
            <p>In order to use InvariantJ, you must have an <a href="http://ant.apache.org/" 
                title="Apache Ant website">Ant</a> build file. During the build of you project, InvariantJ will 
                decorate the byte code of your compiled classes using <a href="http://www.jboss.org/products/javassist" 
                title="Javassist home page">Javassist</a>.</p>
            <p>Download and unzip the latest InvariantJ zip file. Place the contents of the lib directory in a suitable 
                location in your project:</p>
            <ul>
                <li>Javassist is required to be on the build time classpath</li>
                <li>InvariantJ is required to be on the build and run time classpaths</li>
            </ul>
            <p>Now add the following task definition to your build file:</p>
            <ul class="codeBlock">
                <li>&lt;<span class="keyword">taskdef</span> <span class="variable">name</span>="<span 
                    class="string">invariantj</span>" <span class="variable">classname</span>="<span 
                    class="string">com.stateofflow.invariantj.build.InvariantJ</span>"&gt;</li>
                <li>&nbsp;&nbsp;&lt;<span class="keyword">classpath</span>&gt;&#8230;where you put the InvariantJ and 
                    Javassist jars&#8230;&lt;/<span class="keyword">classpath</span>&gt;</li>
                <li>&lt;/<span class="keyword">taskdef</span>&gt;</li>
            </ul>
            <p>Next add a target like the one below (the "<span class="string">compile</span>" target is assumed to be 
                the one that produces the class files to be instrumented):</p>
            <ul class="codeBlock">
                <li>&lt;<span class="keyword">target</span> <span class="variable">name</span>="<span 
                    class="string">instrument</span>" <span class="variable">depends</span>="<span 
                    class="string">init,compile</span>"&gt;</li>
                <li>&nbsp;&nbsp;&lt;<span class="keyword">invariantj</span> <span 
                    class="variable">destdir</span>="<span class="string">&#8230;where you want the instrumented 
                    classes to be written&#8230;</span>"&gt;</li>
                <li>&nbsp;&nbsp;&nbsp;&nbsp;&lt;<span class="keyword">instrumentpath</span>&gt;&#8230;&lt;/<span 
                    class="keyword">instrumentpath</span>&gt;</li>
                <li>&nbsp;&nbsp;&nbsp;&nbsp;&lt;<span class="keyword">classpath</span>&gt;&#8230;&lt;/<span 
                    class="keyword">classpath</span>&gt;</li>
                <li>&nbsp;&nbsp;&lt;/<span class="keyword">invariantj</span>&gt;</li>
                <li>&lt;/<span class="keyword">target</span>&gt;</li>
            </ul>
            <p>Where</p>
            <ul>
                <li><span class="keyword">instrumentpath</span> is a <a 
                    href="http://ant.apache.org/manual/using.html#path" 
                    title="Description of Ant's path-like structures">path-like structure</a> defining the set of files 
                    to be instrumented</li>
                <li><span class="keyword">classpath</span> is a <a href="http://ant.apache.org/manual/using.html#path" 
                    title="Description of Ant's path-like structures">path-like structure</a> defining the classpath 
                    for all classes referenced by those in the <span class="keyword">instrumentpath</span>. If the set 
                    of classes on <span class="keyword">instrumentpath</span> is referentially closed (except for 
                    references to standard Java classes) then this element is optional.</li>
                <li><span class="variable">destdir</span> is the destination directory into which the instrumented 
                    class files will be written</li>
            </ul>
            <p>For a complete example, see <a href="build.xml.txt" title="Example Ant build file">build.xml</a></p>
            <div class="sectionHeading">
                <a name="ide">Using InvariantJ with IDEs</a>
            </div>
            <p>InvariantJ can be used with Integegrated Development Environments such as <a href="http://www.eclipse.org" title="Eclipse homepage">Eclipse</a>
            and <a href="http://www.jetbrains.com/idea/" title="IntelliJ IDEA">IntelliJ IDEA</a> using their Ant integration features.</p>
            <p>For instructions on achieving this with Eclipse, see <a href="eclipse.html" title="Eclipse Ant integration">here</a>. In IntelliJ IDEA,
            the Build tab's context sensitive menu can be used to add an Ant target after a compile.</p>
            <div class="sectionHeading">
                <a name="wherePrecisely">Where Precisely are Invariants Checked</a>
            </div>
            <p>For the purposes of this discussion, constructors should not be considered as methods&nbsp;&#8211; the 
                general term &#8216;behaviour&#8217; denotes both methods and constructors.</p>
            <div class="subSectionHeading"><a name="staticModel">Static Model</a></div>
            <p>The following points specify the static model for invariant checking. Whether invariants are actually 
                checked at each of these points is subject to gating by the <a href="#dynamicModel" 
                title="InvariantJ's Dynamic Model">dynamic model</a> specified below:</p>
            <ul>
                <li>On entry to and exit from <span class="code keyword">public</span> methods, the set of invariants 
                    to be verified consists of those declared in the instance's class and all superclasses</li>
                <li>On exit from <span class="code keyword">public</span> constructors, the set of invariants to be 
                    verified consists of those declared in the class declaring the constructor and all superclasses</li>
                <li>Invariants are not verified at any other locations</li>
            </ul>
            <div class="subSectionHeading">
                <a name="dynamicModel">Dynamic Model</a>
            </div>
            <p>InvariantJ has a dynamic aspect to its behaviour that means that for every thread of execution, an 
                object's class invariants will only be verified at the highest point in the stack that the flow of 
                execution encountered the object and only if the behaviour concerned is <span 
                class="code keyword">public</span>.</p>
            <p>The reason for this is that sending a message to <span class="code keyword">this</span> can reasonably 
                be considered an implementation detail, whether or not the behaviour that intercepts that message is 
                <span class="code keyword">public</span>. The same message originating outside the target object will 
                result in an invariant check however, pursuant to the object not having been the recipient of any 
                messages higher in the stack.</p>
            <p>The argument is a little more tenuous for disabling invariant checking of an object when, for example, 
                the object sends a message to another which sends a message (intercepted by a <span 
                class="code keyword">public</span> method) back to the first. In this case, InvariantJ considers that 
                the two objects are collaborating in some shared work and requires only that the invariants are 
                maintained for each object upon initial entry and final exit.</p>
            <p>It is certainly possible to work with a model of class invariants that is specified entirely by 
                InvariantJ's <a href="#staticModel" title="InvariantJ's Static Model">static model</a> regardless of 
                the dynamic context&nbsp;&#8211; in fact, it would have been far easier to implement InvariantJ this 
                way. However, it is felt that the implementation provided allows the powerful notion of class 
                invariants to be applied without requiring hoops to be jumped through, although it is acknowledged that 
                this imlementation does potentially lose some &#8216;locality&#8217; should a violation occur.</p>
            <p>The single exception to the &#8216;first encounter&#8217; rule is that when constructors are chained, 
                the testing of invariants will occur on exit of <i>every</i> <span class="code keyword">public</span> 
                constructor in the chain. This is due to the requirement expressed in <a 
                href="http://java.sun.com/docs/books/jls/third_edition/html/classes.html#8.8.7" 
                title="Section 8.8.7 of the Java Language Specification: &#8216;Constructor Body&#8217;">section&nbsp;8.8.7</a> 
                of the <a href="http://java.sun.com/docs/books/jls/third_edition/html/j3TOC.html" 
                title="Java Language Specification">Java Language Specification</a> that a constructor must begin with 
                an invocation of a superclass's constructor or another constructor declared in the class. It is 
                therefore not possible for InvariantJ to decorate the bytecode in such a way that it can note that one 
                constructor has been invoked by another. This only has consequences if the chain is between two 
                constructors of the same class (as opposed to chaining a constructor to a superclass constructor), in 
                which case it may be necessary to break the chain and extract the body of the invoked constructor into 
                a non-<span class="code keyword">public</span> behaviour that both constructors in the original chain 
                can use.</p>
            <div class="sectionHeading">
                <a name="versions">Software Versions</a>
            </div>
            <ul>
                <li><a href="http://ant.apache.org/" title="Apache Ant website">Ant</a> - 1.6.2</li>
                <li><a href="http://www.csg.is.titech.ac.jp/~chiba/javassist/" title="Javassist home page">Javassist</a> - 
                    3.7.0.GA (included in the distribution's lib directory)</li>
            </ul>
        </div>
    </body>
</html>